『プログラミング Coq』池渕未来
2011年頃のCoq入門
https://www.iijlab.net/activities/programming-coq/coqt1.html
#形式手法